the_es:event_system{i:l}, e:es-E(the_es).
(es-isrcv(the_es; e))
 (es-index(the_es; e)
 ( int_seg(0; ||es-sends(the_es; es-lnk(the_es; e); es-sender(the_es; e))||)) 

latex

Definitions

t  T, P  Q, x:A. B(x), sender(e), s = t, Type, prop{i:l}, A c B, x:A  B(x), P  Q, pred!(e;e'), left + right, x:AB(x), pred(e), first(e), A, a < b, , {x:A| B(x)} , f(a), x:A. B(x), SWellFounded(R(x;y)), void, isect(A; x.B(x)), False, rcv-from-on(dE; dL; info; e; l; r), type List, subtype(S; T), receives(dE; dL; pred?; info; p; e; l), sends(dE; dL; pred?; info; val; p; e; l), True, rcv(l,tg), IdLnk, ecase1(e;info;i.f(i);l,e'.g(l;e')), P  Q, EOrderAxioms(E;pred?;info), isrcv(k), es_info(es), es-oaxioms(es), es-pred?(es), es-eq(es), es-kind(es; e), es_val(es), es-index(es; e), es-sends(es; l; e), es-sender(es; e), es-lnk(es; e), es-isrcv(es; e), es-E(es), event_system{i:l}, int_seg(i; j), top, link(e), kind(e), lnk(k), sqequal(s; t), rcv?(e), b, idlnk-deq, Id

Lemmas

es-isrcv wf, es-E wf, event system wf, isrcv wf, kind wf, index wf, rcv?-kind, IdLnk wf, false wf, true wf, length-map, receives wf, top wf, rcv-from-on wf, idlnk-deq wf, link wf, nat wf, not wf, first wf, pred wf, assert wf, rcv? wf, sender wf, Id wf